Doctoral Thesis Proposal - Afonso Tinnoco

— 9:30pm

Location:
In Person and Virtual - ET - Gates Hillman 8102 and Zoom

Speaker:
AFONSO TINOCO, Ph.D. Student, Computer Science Department, Carnegie Mellon University
https://cmuportugal.org/students/afonso-tinoco/

Towards Practical and Verifiable Distributed Systems: Applications of Oblivious Algorithms, Garbled Circuits and Formal Methods+

In my research, I want to design and develop practically efficient and provably secure distributed systems. To this end, I combine applied cryptography and formal verification tools. The goal of this proposal is to provide primitives that can be used in distributed systems, as well as methodologies to verify consensus protocols, to ensure the security, efficiency, and correctness of distributed systems. Specifically, the research focuses on three main areas: practical implementations of oblivious algorithms for Trusted Execution Environments (TEEs); practical and verified implementations of Garbled RAM; and methodologies to verify safety and liveness of consensus protocols. 

TEEs can be used to offer efficient crash fault nodes with confidential computations; however, most TEEs implementations leak the page-level memory access pattern to the host machine where the TEE is running. Therefore, to guarantee confidential computations, TEE programs need not only correct implementations but also to be memory trace-oblivious. There has been extensive theoretical research in oblivious algorithms; however, there is a gap with practical implementations, particularly in the TEE setting. In this proposal, we aim to close this gap, providing an oblivious data structure library akin to C++'s STL, and extending it with oblivious graph algorithms. 

TEEs require trust in the hardware manufacturer and a certain level of hardware/software integrity. In scenarios where this isn't possible, Garbled Circuits can be used to provide equivalent secure processor guarantees based on cryptographic assumptions. To achieve an efficient Garbled Circuit processor, Garbled RAM is necessary, and recent theoretical advancements suggest using tristate circuits to implement it. In this proposal, we aim to achieve concretely more efficient Garbled RAM constructions, as well as provide methodologies to verify the correctness of tristate circuits. 

Finally, while TEEs and Garbled RAM aim to achieve secure computations, ensuring the correctness of the underlying protocols that use them is critical. We have previously developed a python DSL to verify safety properties of distributed system protocols. In this proposal, we aim to extend this framework to verify liveness properties of distributed system protocols, focusing on proof automation and generalization.  

Thesis Committee: 

Elaine Shi (Co-chair)
Rodrigo Rodrigues (Co-chair, University of Lisbon, Instituto Superior Técnico)
Bryan Parno
Pedro Adão (University of Lisbon, Instituto Superior Técnico)
José Fragoso (University of Lisbon, Instituto Superior Técnico)
Andrew Miller (University of Illinois Urbana-Champaign)
 

Additional Information

In Person and Zoom Participation. See announcement.

Event Website:
https://csd.cmu.edu/calendar/doctoral-thesis-proposal-afonso-tinnoco